Абелеві категорії

Абелеві категорії — це збагачене поняття категорії Сандерса-Маклейна поняттями нульового обʼєкту, що одночасно ініціальний та термінальний, властивостями існування всіх добутків та кодобутків, ядер та коядер, а також, що всі мономорфізми і епіморфізми є ядрами і коядрами відповідно (тобто норомальними).

def isAbelian (C: precategory): U₁ := Σ (zero: hasZeroObject C) (prod: hasAllProducts C) (coprod: hasAllCoproducts C) (ker: hasAllKernels C zero) (coker: hasAllCokernels C zero) (monicsAreKernels: Π (A S: C.C.ob) (k: C.C.hom S A), Σ (B: C.C.ob) (f: C.C.hom A B), isKernel C zero A B S f k) (epicsAreCoKernels: Π (B S: C.C.ob) (k: C.C.hom B S), Σ (A: C.C.ob) (f: C.C.hom A B), isCokernel C zero A B S f k), U

Мотивація

Ось п’ять коротких формальних застосувань математичного апарату абелевих категорій:

Гомологічна алгебра: абелеві категорії забезпечують основу для гомологічної алгебри, яка є розділом алгебри, що вивчає властивості груп гомології та когомології. Теорія похідних функторів, яка є фундаментальним інструментом гомологічної алгебри, базується на понятті абелевої категорії.

Алгебраїчна геометрія: абелеві категорії використовуються в алгебраїчній геометрії для вивчення когомологій пучка, що є потужним інструментом для розуміння геометричних властивостей алгебраїчних многовидів. Зокрема, категорія пучків абелевих груп на топологічному просторі є абелевою категорією.

Теорія представлень: абелеві категорії природно виникають у вивченні теорії представлень, яка є розділом математики, який має справу з алгебраїчними структурами, що виникають під час вивчення симетрії. Категорія модулів над кільцем, наприклад, є абелевою категорією.

Топологічна квантова теорія поля: абелеві категорії відіграють центральну роль у вивченні топологічної квантової теорії поля, яка є розділом математичної фізики, що має справу з математичною структурою топологічних просторів. У цьому контексті абелеві категорії виникають як категорії граничних умов для певних типів теорій топологічного поля.

Теорія категорій: Нарешті, абелеві категорії є важливим об’єктом дослідження в теорії категорій, яка є розділом математики, який вивчає властивості категорій та їхні зв’язки. Зокрема, абелеві категорії забезпечують природне середовище для вивчення властивостей адитивних функторів, які є фундаментальним інструментом у теорії прохідних категорій та функторів. Тут можна порадити роботу румунських математиків Бакура і Деляну «Вступ в теорію категорій та функторів».

.

Джерела

Поняття абелевої категорії вперше було введено математиком Александром Гротендіком у його основоположній статті «Sur quelques points d'algèbre homologique» (Про деякі аспекти гомологічної алгебри), опублікованій у 1957 році. Гротендік представив абелеві категорії як спосіб об’єднання вивчення гомологічної алгебри в різних математичних дисциплінах, таких як алгебраїчна геометрія, алгебраїчна топологія та теорія представлень.

У цій статті Гротендік визначив абелеву категорію як категорію, яка задовольняє ряду аксіом, включаючи існування ядер і коядер, теореми ізоморфізму та існування точних послідовностей. Він показав, що багато категорій алгебраїчних об'єктів, таких як категорії модулів над кільцем або пучків абелевих груп на топологічному просторі, є абелевими категоріями.

З тих пір концепція абелевих категорій стала фундаментальним інструментом у багатьох областях математики, включаючи алгебраїчну геометрію, теорію представлень, гомологічну алгебру та теорію категорій. Він також застосовувався в таких галузях фізики, як топологічна квантова теорія поля.

Визначення

При формальній побудові абелевих категорій потрібно розділяти типову сигнатурну інформацію абстрактної абелевої категорії та її інстанціацій, таких як категорія абелевих груп, модулів над кільцем, тощо.

Всі, хто хоче побачити сучасні абелеві категорії в кубічній Агді, може подивитися магістерську роботу 2021 року Девіда Еліндера «Дослідження абелевих категорій і унівалентній теорії типів».

module abelian where import lib/mathematics/categories/category import lib/mathematics/homotopy/truncation def zeroObject(C: precategory) (X: C.C.ob): U₁ := Σ (bot: isInitial C X) (top: isTerminal C X), U def hasZeroObject (C: precategory) : U₁ := Σ (ob: C.C.ob) (zero: zeroObject C ob), unit def hasAllProducts (C: precategory) : U₁ := Σ (product: C.C.ob -> C.C.ob -> C.C.ob) (π₁: Π (A B : C.C.ob), C.C.hom (product A B) A) (π₂: Π (A B : C.C.ob), C.C.hom (product A B) B), U def hasAllCoproducts (C: precategory) : U₁ := Σ (coproduct: C.C.ob -> C.C.ob -> C.C.ob) (σ₁: Π (A B : C.C.ob), C.C.hom A (coproduct A B)) (σ₂: Π (A B : C.C.ob), C.C.hom B (coproduct A B)), U def isMonic (P: precategory) (Y Z : P.C.ob) (f : P.C.hom Y Z) : U := Π (X : P.C.ob) (g1 g2 : P.C.hom X Y), Path (P.C.hom X Z) (P.P.∘ X Y Z g1 f) (P.P.∘ X Y Z g2 f) -> Path (P.C.hom X Y) g1 g2 def isEpic (P : precategory) (X Y : P.C.ob) (f : P.C.hom X Y) : U := Π (Z : P.C.ob) (g1 g2 : P.C.hom Y Z), Path (P.C.hom X Z) (P.P.∘ X Y Z f g1) (P.P.∘ X Y Z f g2) -> Path (P.C.hom Y Z) g1 g2 def kernel (C: precategory) (zero: hasZeroObject C) (A B S: C.C.ob) (f: C.C.hom A B) : U₁ := Σ (k: C.C.hom S A) (monic: isMonic C S A k), unit def cokernel (C: precategory) (zero: hasZeroObject C) (A B S: C.C.ob) (f: C.C.hom A B) : U₁ := Σ (k: C.C.hom B S) (epic: isEpic C B S k), unit def isKernel (C: precategory) (zero: hasZeroObject C) (A B S: C.C.ob) (f: C.C.hom A B) (k: C.C.hom S A) : U₁ := Σ (ker: kernel C zero A B S f), Path (C.C.hom S A) ker.k k def isCokernel (C: precategory) (zero: hasZeroObject C) (A B S: C.C.ob) (f: C.C.hom A B) (k: C.C.hom B S) : U₁ := Σ (coker: cokernel C zero A B S f), Path (C.C.hom B S) coker.k k def hasKernel (C: precategory) (zero: hasZeroObject C) (A B: C.C.ob) (f: C.C.hom A B) : U₁ := ‖_‖₋₁ (Σ (monic: isMonic C A B f), unit) def hasCokernel (C: precategory) (zero: hasZeroObject C) (A B: C.C.ob) (f: C.C.hom A B) : U₁ := ‖_‖₋₁ (Σ (epic: isEpic C A B f), unit) def hasAllKernels (C : precategory) (zero: hasZeroObject C) : U₁ := Σ (A B : C.C.ob) (f : C.C.hom A B), hasKernel C zero A B f def hasAllCokernels (C : precategory) (zero: hasZeroObject C) : U₁ := Σ (A B : C.C.ob) (f : C.C.hom A B), hasCokernel C zero A B f

Абелеві категорії забезпечують природну основу для вивчення гомологічної алгебри, яка є розділом алгебри, що має справу з алгебраїчними властивостями груп гомологій та когомологій. Зокрема, абелеві категорії створюють сеттінг, де можна визначити поняття похідних категорій і похідних функторів.

Основна ідея похідних категорій полягає в тому, щоб ввести нову категорію, яка побудована з абелевої категорії шляхом «інвертування» певних морфізмів, майже так само, як будується поле часток на області цілісності. Похідна категорія абелевої категорії фіксує «правильне» поняття гомологічних і когомологічних груп і забезпечує потужний інструмент для вивчення алгебраїчних властивостей цих груп.

Похідні функтори є фундаментальним інструментом гомологічної алгебри, і їх можна визначити за допомогою концепції похідної категорії. Основна ідея похідних функторів полягає в тому, щоб взяти функтор, який визначено в абелевій категорії, і «підняти» його до функтора, який визначений у похідній категорії. Похідний функтор потім використовується для обчислення вищих груп гомології та когомології об’єктів в абелевій категорії.

Використання похідних категорій і функторів зробило революцію у вивченні гомологічної алгебри, і це призвело до багатьох важливих застосувань в алгебраїчній геометрії, топології та математичній фізиці. Наприклад, похідні категорі використовувалися для доведення фундаментальних результатів алгебраїчної геометрії, таких як знаменита теорема Гротендіка-Рімана-Роха. Вони також використовувалися для вивчення дзеркальної симетрії в теорії суперструн.

.
˙